|
|
Refactoring and Verification of the Code of mkfs xfs
Ťulák, Jan ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work describes the processes of refactoring mkfs.xfs program for a purpose of refining its code and cleaning the technical debt accumulated over 20 years of the program’s existence. The mkfs.xfs source code is then a subject to static analysis and the used tools (CppCheck, Coverity, Codacy, GCC, Clang) are compared in terms of the number and type of the found defects.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (oponent) ; Radu, Iosif (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis focuses on improving the state of the art of automata-based formal analysis and verification techniques for systems with an infinite state space. In the first part of the thesis, we develop two efficient decision procedures for the WS1S logic, both of them exploiting the correspondence between formulae of WS1S logic and finite automata. We start by proposing a novel antichain-based decision procedure which is, however, limited to formulae in the prenex normal form. Later, we generalize the approach to arbitrary formulae by defining the so-called language terms and constructing an on-the-fly procedure dealing with the terms using lazy techniques. In order to achieve an efficient implementation, we propose numerous optimizations (some of these optimization are not limited to our approaches only). We evaluated both our methods with other recent state-of-the art tools. The achieved results are encouraging and show we can extend the usage of WS1S to wider classes of formulae. The second part of the thesis focuses on resource bounds analysis of heap-manipulating programs. We propose a new class of shape norms based on lengths of paths between distinct points in the heap, which we derive automatically from the analysed program. For this class of norms, we introduce a calculus capable of precisely inferring changes of the analysed norms and use it to generate a corresponding integer representation of an input program followed by dedicated state-of-the art resource bounds analysis. We implemented our approach over the shape analysis based on forest-automata, implemented in the Forester tool, and using a well-established resource bounds analyser, implemented in the Loopus tool. In our experimental evaluation, we show that we indeed obtained a powerful analyser that is able to handle some showcase examples that were never analysed fully automatically before.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (oponent) ; Radu, Iosif (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis focuses on improving the state of the art of automata-based formal analysis and verification techniques for systems with an infinite state space. In the first part of the thesis, we develop two efficient decision procedures for the WS1S logic, both of them exploiting the correspondence between formulae of WS1S logic and finite automata. We start by proposing a novel antichain-based decision procedure which is, however, limited to formulae in the prenex normal form. Later, we generalize the approach to arbitrary formulae by defining the so-called language terms and constructing an on-the-fly procedure dealing with the terms using lazy techniques. In order to achieve an efficient implementation, we propose numerous optimizations (some of these optimization are not limited to our approaches only). We evaluated both our methods with other recent state-of-the art tools. The achieved results are encouraging and show we can extend the usage of WS1S to wider classes of formulae. The second part of the thesis focuses on resource bounds analysis of heap-manipulating programs. We propose a new class of shape norms based on lengths of paths between distinct points in the heap, which we derive automatically from the analysed program. For this class of norms, we introduce a calculus capable of precisely inferring changes of the analysed norms and use it to generate a corresponding integer representation of an input program followed by dedicated state-of-the art resource bounds analysis. We implemented our approach over the shape analysis based on forest-automata, implemented in the Forester tool, and using a well-established resource bounds analyser, implemented in the Loopus tool. In our experimental evaluation, we show that we indeed obtained a powerful analyser that is able to handle some showcase examples that were never analysed fully automatically before.
|
|
| |
|
|
Refactoring and Verification of the Code of mkfs xfs
Ťulák, Jan ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work describes the processes of refactoring mkfs.xfs program for a purpose of refining its code and cleaning the technical debt accumulated over 20 years of the program’s existence. The mkfs.xfs source code is then a subject to static analysis and the used tools (CppCheck, Coverity, Codacy, GCC, Clang) are compared in terms of the number and type of the found defects.
|
|
|
Architektonická skulptura chrámu Matky Boží před Týnem na Starém městě pražském v lucemburském období
Peroutková, Jana ; Royt, Jan (vedoucí práce) ; Hlobil, Ivo (oponent)
Magisterská práce zabývající se architektonickou skulpturou chrámu Matky Boží před Týnem v lucemburském období je postavena na základech práce bakalářské, jež zhodnotila dostupnou odbornou literaturu především českých badatelů, prameny, restaurátorské zprávy a stavebně historické průzkumy zabývající se touto památkou. Téma bakalářské práce zaměřené zejména na ikonografické souvislosti zdobných konzol severního bočního portálu chrámu nová studie rozšiřuje na celý soubor kamenné skulptury chrámu sledovaného období. Práce si klade za cíl zhodnocení dostupné zahraniční literatury, revizi ikonografie, stylové roviny a datování celého souboru, a to i na základě spolupráce na nově otevřeném stavebně-historickém průzkumu vedeném NPÚ. Následně bude sochařský soubor Týnského chrámu podroben komparaci s dobově a stylově příbuznými památkami v Čechách i zahraničí. Práce se zaměří na formální, stylovou a ikonografickou analýzu, novou archivní rešerši, na obnovený stavebně-historický a restaurátorský průzkum. Cílem magisterské práce je revize datace, stylové a ikonografické roviny památky, která svým nesourodým výrazem dala prostor k velmi odlišným uměleckohistorickým hodnocením.
|
|
| |
host ::
RSS.